1. Field
The present invention generally relates to electronic design automation. More specifically, the present invention relates to techniques and systems for optimizing a circuit design for formal circuit verification.
2. Related Art
Describing a circuit using a high-level hardware description language allows hardware engineers to define the circuit's functionality and to optimize the circuit's architecture before converting the high-level description into a detailed physical layout for the circuit.
The goal of circuit verification is to determine whether the circuit is expected to behave as desired under normal operating conditions. A circuit can be verified using different techniques which include formal verification techniques, simulation-based verification techniques, and hybrid verification techniques which combine elements of both formal verification techniques and simulation-based verification techniques.
Formal verification techniques attempt to prove that the circuit under verification (CUV) will behave as desired during operation. Formal verification techniques typically utilize two types of logical conditions: assumptions and assertions. Assumptions are logical conditions that are used to model the runtime environment, and assertions are logical conditions that define the desired behavior of the CUV. Unfortunately, it can sometimes be computationally impractical to formally verify circuits that are large and complex.
Simulation-based verification techniques simulate the CUV to ensure that the CUV is behaving as desired. Compared to formal verification, simulation usually requires fewer computational resources. Unfortunately, simulation-based verification techniques usually cannot guarantee that the CUV will behave as desired because it is usually impractical to cover the entire state space.
In a hybrid verification technique, the verification tool can simulate the CUV, and when the circuit reaches a state that is of interest, the tool can formally verify assertions for the CUV. Hybrid verification techniques can provide the best of both worlds: they require fewer computational resources than formal verification techniques, and they are more rigorous than simulation-based verification techniques.
Regardless of which circuit verification technique is used, a significant portion of the time-to-market is usually spent on verifying the circuit. Hence, it is desirable to improve the performance of verification tools because it can have a dramatic impact on the time-to-market.